ABS: k(v) sends [tg,f(State(ds), v)] on l

STM: Rusends1 wf

ABS: (L)

STM: Rlist wf

ABS: xL.R(x)

STM: Rall wf

STM: Rall-cons

STM: Rall-nil

STM: es realizer-subtype

ABS: pr |= X

STM: sem-sat wf

ABS:  X

STM: sem-satisfiable wf

ABS: K-sem(S;equiv)

STM: K-sem wf

ABS: kpr |= X

STM: K-sem-sat wf

ABS: pr implements kpr

STM: K-implements wf

STM: K-refine

ABS: []!P

STM: box! wf

STM: Rplus-implies

STM: Rnone-implies

ABS: R-size(R)

STM: R-size wf

STM: R-size-implies

STM: R-size-base

STM: R-size-decreases

STM: Rnone?-implies

ABS: R-loc(R)

STM: R-loc wf

ABS: R-has-loc(R;i)

STM: R-has-loc wf

STM: R-has-loc-base

STM: R-has-loc-Rplus

STM: Rlist-has-loc

STM: Rall-has-loc

ABS: Rds(R)

STM: Rds wf

ABS: R-ds(R;i)

STM: R-ds wf

STM: R-ds-Rds

ABS: Rda(R)

STM: Rda wf

ABS: R-da(R;i)

STM: R-da wf

STM: R-da-Rlist

STM: R-da-Rda

STM: R-da-Rall

ABS: base-domain-type(n)

STM: base-domain-type wf

ABS: p = q

STM: eq bd wf

STM: assert-eq-bd

ABS: R-base-domain(R)

ABS: R-frame-compat(A;B)

STM: R-frame-compat wf

STM: R-frame-compat-self

STM: R-base-domain wf

ABS: R-interface-compat(A;B)

STM: R-interface-compat wf

ABS: A || B

STM: R-compat wf

ABS: R-icompat(A;B)

STM: R-icompat wf

ABS: R-interface(A;B)

STM: R-interface wf

STM: R-interface-Rplus

STM: R-interface-Rplus2

STM: R-compat-Rplus-sq

STM: R-compat-Rplus2

STM: R-compat-symmetry

STM: R-compat-none

STM: R-compat-Rall

STM: R-compat-Rall2

ABS: R-Feasible(R)

STM: R-Feasible wf

STM: R-Feasible-Rplus

STM: Rplus-Feasible

ABS: R-self-interface(R)

STM: R-self-interface wf

STM: R-self-interface-implies

STM: R-Feasible-self-interface

STM: R-interface-compat-self

STM: R-compat-self

STM: R-Feasible-effect

ABS: A  B

STM: R-sub wf

STM: R-sub-lemma1

STM: R-sub-self

STM: R-sub-plus-left

STM: R-sub-plus-right

STM: R-sub transitivity

STM: R-sub-compat

STM: R-sub-feasible

STM: R-sub-Rlist

STM: R-feasible-Rlist

STM: R-feasible-Rall

STM: R-compat-Rlist

ABS: P holds in state init  e@i

STM: pre-init-p wf

ABS: pre-init-p2(es;i;ds;init;a;T;P)

STM: pre-init-p2 wf

ABS: R-state(R;i)

STM: R-state wf

STM: R-state-plus-cap

STM: R-Feasible-state

STM: Rinit-compat

STM: Rframe-compat

ABS: R-occurs(R;i;z)

STM: R-occurs wf

STM: R-occurs-has-loc

ABS: write-restricted(R;i;k)

STM: write-restricted wf

STM: write-restricted-has-loc

ABS: read-restricted(R; i; y)

STM: read-restricted wf

STM: read-restricted-R-occurs

STM: read-restricted-has-loc

STM: not-R-occurs-frame-compat

STM: not-R-occurs-init-compat

STM: dom-R-ds-occurs

STM: not-R-has-loc-R-ds

STM: not-R-has-loc-R-da

STM: R-compat-disjoint

ABS: R-lnk-tags(ds;da;l;tgs;ks;g)

STM: R-lnk-tags wf

STM: R-lnk-tags-compat2

STM: Rinit-lnk-tags-compat

STM: R-lnk-tags-loc

STM: R-lnk-tags-da

STM: R-compat-ds

STM: R-compat-da

STM: R-compat-da2

STM: R-interface-icompat

STM: R-interface-iff

STM: R-interface-iff2

STM: R-icompat-one-loc

STM: R-icompat-one-loc2